Nuprl Lemma : isect2_wf
4,23
postcript
pdf
T1
,
T2
:Type.
T1
T2
Type
latex
Definitions
T1
T2
,
,
if
b
t
else
f
fi
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
ifthenelse
wf
,
bool
wf
origin
T1, T2:Type. T1 
T2 
Type T1, T2:Type. T1 T2 Type T2
t else f fix:A. B(x) T